(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(declare-fun d (Int) Bool)
(declare-fun e (Int) Bool)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-fun h (Int) Bool)
(declare-fun i (Int) Bool)
(declare-fun j (Int) Bool)
(declare-fun k (Int) Bool)
(declare-fun l (Int) Bool)
(declare-fun m (Int) Bool)
(declare-fun n (Int) Int)
(check-sat)
(assert (= (= (g 0) 1) (l 0)))
(assert (= (n 1) 0))
(assert (let ((n (g 1))) (let ((r (+ 2 n))(s 0)(m (l 0))) (let ((ab (ite m 0 n))(t (e 0))) (let ((u (ite t ab s))(v 0)(w (j 0))) (let ((x (ite w v n))(y (d 0))) (let ((z (ite y x u))(ac (i 0))) (let ((ad (ite ac r n))(ae (c 0))) (let ((af (ite ae ad z))(ag (= a 0))) (let ((ah (ite ag 0 af))(ai (g 2))) (= ai ah)))))))))))
(assert (let ((aj (n 0))(ak 0)(al 0)(am (k 0))) (let ((an (ite am al aj))(ao (m 0))) (let ((ap (ite ao an ak))(aq 0)(ar (d 1))) (let ((ay (ite ar aq ap))(bj 0)(at (b 0))) (let ((au (ite at bj ay))(av (= a (- 1)))) (let ((aw (ite av 7 au))(ax (n 0))) (= ax aw))))))))
(assert (<= 1 (n 0)))
(assert (let ((az (f 0))) (let ((ba (<= 1 az))) (let ((bb (and ba))(bc (g 0))) (let ((bd (= bc 0))) (let ((be (and bd bb))(aj (n 2))) (let ((bf (= aj 0))) (let ((bg (and bf be))(bh (h 0))) (= bh bg)))))))))
(check-sat)
